FDL - Step of Proof: or_false

Step of Proof: or_false_l

9,38

Inference at *
Iof proof for Lemma or false l:

. (False

by ((((RepD)

CollapseTHENM (ProveProp1))

)

CollapseTHENA ((Auto_aux (first_nat 1:n

C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

Definitions t T, P Q, P Q, P Q, P Q, P Q, , x:A. B(x), False

Lemmas false wf

Definitions	t T, P Q, P Q, P Q, P Q, P Q, , x:A. B(x), False
Lemmas	false wf